Nuprl Lemma : free-from-atom-outl 11,40

A:Type, x:(A + Top), a:Atom1. x:A + Top||a  (isl(x))  outl(x):A||a 
latex


Definitionst  T, outl(x), P  Q, x:AB(x), , False, if b then t else f fi , ff, tt, isl(x), b
Lemmastop wf, free-from-atom wf1, isl wf, assert wf

origin